Nuprl Lemma : fifoSender-antecedent
11,40
postcript
pdf
es
:ES,
ff
:FIFO,
i
:
ff
.C.
e
.
j
:
ff
.C. (
ff
.S(
j
,
i
,
e
))
ff
.Sender(
i
)
e
.
ff
.R(
i
,
e
)
latex
Definitions
x
:
A
B
(
x
)
,
ff
.R
,
ff
.C
,
ff
.S
,
ff
.Sender
,
let
a
,
b
,
c
,
d
,
e
,
f
,
g
=
u
in
v
(
a
;
b
;
c
;
d
;
e
;
f
;
g
)
,
FIFO
,
t
T
,
ES
,
x
:
A
.
B
(
x
)
,
Q
f
P
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
f
(
a
)
,
for clients
C
sends FIFO from j to i via (
S
[j,i],
codes
) receives at i via (
R
[i],
decodes
)
,
x
.
A
(
x
)
,
(state when
e
)
,
Type
,
P
Q
,
e
c
e'
,
P
&
Q
,
,
s
=
t
,
{
x
:
A
|
B
(
x
)}
,
E
,
t
.1
,
Q
f
P
,
(
e
<
e'
)
,
b
Lemmas
es-causle
wf
,
es-state-when
wf
,
antecedent-surjection
wf
,
es-E
wf
,
event
system
wf
,
FIFO
wf
origin
es:ES, ff:FIFO, i:ff.C. 
e.
j:ff.C. (ff.S(j,i,e)) 
ff.Sender(i) e.ff.R(i,e) es:ES, ff:FIFO, i:ff.C. e.j:ff.C. (ff.S(j,i,e)) ff.Sender(i) e.ff.R(i,e) 
B(x)
T
B(x)
Q
e'
b